Nuprl Lemma : gcd_p_neg_arg_a
2,24
postcript
pdf
a
,
b
,
y
:
. GCD(
a
;
b
;
y
)
GCD(-
a
;
b
;
y
)
latex
Definitions
P
Q
,
GCD(
a
;
b
;
y
)
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
gcd
p
sym
,
gcd
p
neg
arg
,
gcd
p
wf
origin
a, b, y:
. GCD(a;b;y) 
GCD(-a;b;y) a, b, y:. GCD(a;b;y) GCD(-a;b;y) Qx:A. B(x)
T